Signature Fact

暗黙の限量により簡潔に書ける

ただし、Factで書いた場合のどういう式と等価であるかはちゃんと理解してないとミスる

以下の2つは等価

Signature Factで記述

code:alloy

sig S {...} { F }

code:alloy

sig S {...}

fact { all this: S | F" }

例

以下の2つは等価

code:alloy

sig Host {}

sig Link { from, to: Host }

fact { all x: Link | x.from != x.to }

code:alloy

sig Host {}

sig Link { from, to: Host } { from != to }